Automated Theorem Proving in Temporal Logic:T-Resolution

This paper presentes a novel resolution method,T-resolution,based on the first order temporal logic.The primary claim of this method is its soundness and completeness.For this purpose,we construct the corresponding semantic trees and extend Herbrand‘s Theorem.     

ELNF演算的解释技术

ＥＬＮＦ演算是我们在ＬＮＦ演算的基础上扩充逻辑程序设计能力而得到的一种函数／逻辑演算系统，它构成了作者设计的函数／逻辑语言ＲＦＵＮＬＯＧ的基础．本文介绍ＥＬＮＦ演算的解释实现技术，包括数据结构、系统结构以及各个模块的设计思想．最后给出了在此解释系统下，几个典型程序的运行时间．     

FP──VLSI自动综合系统

ＦＰ—ＶＬＳＩ自动综合系统是一个集成化的ＶＬＳＩ自动设计工具，它能完成从并行算法到脉动算法到脉动结构再到逻辑结构最后到ＣＭＯＳ版图的自动综合过程．ＦＰ—ＶＬＳＩ系统以脉动阵列为ＶＬＳＩ的体系结构，采用具有良好代数性质的ＦＰ／Ｂ语言作为各层次的描述语言，通过程序变换进行综合和优化．该系统支持形式化的ＶＬＳＩ设计方法，能保证设计结果的正确性．     

Chrestenson函数序列的生成方法及其数学分析

本文提出了适于三种序号的Ｃｈｒｅｓｔｅｎｓｏｎ函数序列的复制方法，对其复制过程进行了数学分析，并指出当Ｃｈｒｅｓｔｅｎｓｏｎ函数退化为Ｗａｌｓｈ函数时，此方法即为复制理论中的平移复制方法。     

FSM状态间逻辑条件检验的算法研究

有限状态机(FSM)是VLSI控制结构的一种映射,它的自动综合成为设计自动化的一个十分重要的环节和途径。本文讨论在FSM自动综合中输入阶段的状态间逻辑条件检验的问题,研究分析状态间逻辑条件检验的相互关系及影响,并提出了FSM状态间逻辑条件检验的优化算法,从而使时间复杂度降低,实现更加简便。最后,本文给出了优化算法的流程和一些实验结果,结果令人满意。     

逻辑程序部分演绎系统的研制

介绍了如何实现一个自动化的逻辑程序部分演绎系统，在逻辑程序部分演绎的理论基础上给出该部分演绎系统的控制结构，并分模块描述了它们的功能和实现技术，特别对核心模块──程序部分演绎模块的算法作了较为详细的分析，最后讨论了计算规则和程序改名变形方法对部分演绎结果程序执行效率的影响。     

半导体激光双稳态光逻辑和信号处理

利用光纤耦合输出反馈泵浦半导体激光双稳器件,实现了微分增益、反微分增益、双稳、反双稳和零偏等5种工作模式的运转,完成了5种基本光逻辑和光信号限幅,整形和脉冲触发等光信号处理功能。     

2、3号炉自动控制系统在DCS上的逻辑改进

对2、3号炉自动控制系统在DCS改造中遇到的诸多问题进行分析，并提出了解决问题的方法，提高了自动投入率。     

基于图形处理离散事件系统监控阻塞的新方法

本文提出了一种基于图形处理监控阻塞问题(SCPB)的新方法,用该方法可有效、直观地分析、求解SCPB。为此,本文给出了改进满意程度(SM)和阻塞程度(BM)的几种方法,并指出了这些方法的特性,从而得以同时改进SM和BM,并优化现有的监控器。